Make the repo's licensing single and consistent, matching the wokelangiser
reference policy and the merged iseriser pattern:

- Remove contradictory PMPL-1.0-or-later / Palimpsest self-claims from README
  badges/footers, QUICKSTART, RSR_OUTLINE, STATE-VISUALIZER, and machine-readable
  governance (META, stapeln, deny.toml allow-list, copilot/AGENTIC SPDX
  directives, Trust/Must LICENSE-content checks, per-project CLAUDE.md).
- Encode the docs split in REUSE dep5: *.adoc/*.md/docs/** -> CC-BY-SA-4.0,
  everything else -> MPL-2.0.
- READMEs show MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges; full texts live in
  LICENSES/; root LICENSE stays MPL-2.0 for GitHub's licence chip.

Preserves legitimate non-self references: cargo-deny's AGPL deny-list, the
"never use AGPL" estate policy, and the Contributor Covenant CoC.

Verified: standards/scripts/check-licence-consistency.sh passes; no residual
PMPL/Palimpsest self-claims remain.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

…hapeliser ABI

The chapeliser ABI modules (Types/Layout/Foreign) already compiled under
Idris2 0.7.0 from the prior slice (no holes, paddingFor via `minus`,
thisPlatform = Linux, DecEq off-diagonal cases handled). This adds the
missing buildable-package wiring and a genuine theorem module.

Changes:
- Add src/interface/abi/chapeliser-abi.ipkg listing all four ABI modules
  (Chapeliser.ABI.{Types,Layout,Foreign,Proofs}) with sourcedir = ".".
- Add src/interface/abi/Chapeliser/ABI/Proofs.idr with machine-checked
  theorems over the ABI's real distributed-computation types:
  * Result-code encoding pins (okIsZero, nullPointerIsFour,
    retryExhaustedIsFive, checkpointErrorIsSix).
  * Slice-descriptor layout pins, incl. countOffset = startOffset + 8
    (no padding between the two u64s).
  * Default checkpoint layout pins (64-byte tag, 1 MiB data).
  * Partition completeness + disjointness => ValidPartition for two
    concrete explicit partitions (10/2 and 10/3). Witnesses are built
    from explicit slice vectors because perItemSlices routes through
    Nat div/mod, which does not reduce during conversion checking.
  * Gather conservation (invariant #2) for [3,3,4] => 10 and [] => 0.
  * Serialisation round-trip witnesses (Bincode, Raw).
  * Retry isolation (invariant #4) and item-buffer isolation/offset pins.
- .gitignore: add **/build/, *.ttc, *.ttm so nested Idris2 build artifacts
  (src/interface/abi/build) are never committed.

Build is clean: `cd src/interface/abi && idris2 --build chapeliser-abi.ipkg`
exits 0 with zero errors and zero warnings. No believe_me/assert_total/
postulate/holes anywhere; all obligations discharged genuinely.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

Adversarial review found two ABI theorems were vacuously inhabited:

- PartitionComplete's `IsComplete` bound a fresh free implicit `n`,
  disconnected from the partition index, so `IsComplete Refl` typechecked
  for ANY partition (it solved n := sliceSum slices). Bind {n}{k}{p} in the
  constructor so the obligation `sliceSum p.slices = n` is tied to the
  declared item count. The existing complete partitions (4+6=10, 3+3+4=10)
  still prove; an incomplete one (sum 9, n=10) is now correctly rejected.
- RoundTrip accepted every format unconditionally. Re-index it on
  (origLen, decodedLen) with a real obligation `decodedLen = origLen`
  (the byte-length invariant that crosses the FFI). A length mismatch
  (RoundTrip Bincode 128 64) is now uninhabited.

Verified: idris2 --build chapeliser-abi.ipkg clean (0 errors/warnings);
negative controls for both theorems fail to typecheck as required.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA